Due to consumers' increasing expectation of longer battery life and higher performance for their mobile devices, power management has become one of the most critical design issues. However, as integrated circuits move into nanometer-scale processes, devices created using 90-nanometer and smaller process technologies can consume as much power when they are not in use as when they are being used because of increased leakage current when the devices are in the idle state. Minimizing leakage current and optimizing dynamic power consumption can lead to longer battery life and lower packaging and cooling costs. While advanced low power design methodologies, such as static and dynamic voltage/frequency scaling, power gating, and state retention, offer additional power savings, they also increase the complexity of design verification.
The complexity of design verification is exacerbated by the fact that the majority of the low power logic is introduced into the gate netlist during synthesis and physical implementation. However, a full-chip exhaustive gate-level simulation is not a practical or scalable methodology for verifying the functionalities of today's complex designs. In recent years, verification methodology utilizing formal (mathematical) proofs has gained wide popularity due to their ability to verify complex designs exhaustively. Equivalence checking (EC) is one such formal verification method which allows checking the logical equivalence of two designs at the same or different-levels of abstraction. For instance, EC can check whether an implemented full-chip gate netlist is equivalent to the reference full-chip RTL design.
FIG. 1A illustrates a conventional method for conducting equivalence checking. As shown in FIG. 1A, the method compares a design specification represented by an RTL netlist 102 to a design implementation represented by a gate netlist 106. The gate netlist 106 is created from the RTL netlist 102 by using a synthesis tool 104. In general, an EC methodology utilizes formal verification techniques such as Binary Decision Diagrams (BDDs) and Satisfiability (SAT) Solvers that operate on the Boolean gate level netlist to establish the equivalence between the RTL netlist 102 and the gate netlist 106 of a design. One drawback of this conventional methodology is that no low power logic is included in the RTL netlist and the gate netlist, and thus the EC does not verify any low power logic that may be used in the ultimate design.
FIG. 1B illustrates another conventional method for conducting equivalence checking. This method modifies the conventional method described in FIG. 1A by incorporating synthesis-tool specific low power commands 103 in the generation of the gate netlist. Thus the synthesis tool 104 uses both the RTL netlist and the synthesis-specific low power commands to generate a low power gate netlist 108. Then, the EC is conducted between the design specification represented by the RTL netlist 102 and the design implementation represented by the low power gate netlist 108. There are at least two drawbacks associated with this approach. First, the low power logic in the gate netlist cannot be verified since there is no low power logic in the original RTL netlist. Second, performing EC between RTL netlist and low power gate netlist without disabling the low power logic in gate netlist may yield incorrect verification results. The reason is that the low power logic inserted in the gate netlist by the synthesis-specific commands, such as isolation cell logic, state retention cell logic etc., is shared with the normal operation logic, and can alter the functionality of the design in the normal operating modes. In order to perform EC of normal operating mode (between RTL netlist and low power gate netlist), certain constraints need to be manually added to the low power gate netlist. These constraints tie certain signals in the design (pins or nets) to logic 0 or logic 1 value, thereby allowing disabling the low power logic. The process of applying such hard-coded (0 or 1) constraints to the gate netlist is very tedious and prone to human errors. Furthermore, applying multiple pin or net constraints on the low power gate netlist may cause certain valid functional modes to be excluded from the formal verification process, thereby resulting in incomplete verification.
Therefore, there is a need to address the issues associated with the conventional equivalence checking methodologies for a low power design.